\begin{tabbing}
msga\{i:l\}
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=${\it ds}$:$x$:Id fp$\rightarrow$ Type\{i\}\+
\\[0ex]$\times$ (${\it da}$:$a$:Knd fp$\rightarrow$ Type\{i\}
\\[0ex]$\times$ ${\it init}$:$x$:Id fp$\rightarrow$ $\mathbb{Q}\rightarrow$fpf{-}cap(${\it ds}$;IdDeq;$x$;Void)
\\[0ex]$\times$ ${\it pre}$:$a$:Id fp$\rightarrow$ State(${\it ds}$)$\rightarrow\mathbb{B}$
\\[0ex]$\times$ ${\it ef}$:${\it kx}$::Knd $\times$ Id fp$\rightarrow$ State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;${\it kx}$.1)$\rightarrow\mathbb{Q}\rightarrow$fpf{-}cap(${\it ds}$;IdDeq;${\it kx}$.2;Void)
\\[0ex]$\times$ ${\it send}$:\=${\it kl}$::Knd $\times$ IdLnk fp$\rightarrow$\+
\\[0ex](${\it tg}$:Id
\\[0ex]$\times$ \=(State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;${\it kl}$.1)$\rightarrow$\+
\\[0ex](fpf{-}cap(${\it da}$;KindDeq;rcv(${\it kl}$.2,${\it tg}$);Void) List))) List
\-\-\\[0ex]$\times$ ${\it frame}$:$x$:Id fp$\rightarrow$ Knd List
\\[0ex]$\times$ ${\it sframe}$:${\it ltg}$::IdLnk $\times$ Id fp$\rightarrow$ Knd List
\\[0ex]$\times$ ${\it aframe}$:$k$:Knd fp$\rightarrow$ Id List
\\[0ex]$\times$ ${\it bframe}$:$k$:Knd fp$\rightarrow$ IdLnk List
\\[0ex]$\times$ ${\it rframe}$:$x$:Id fp$\rightarrow$ Knd List
\\[0ex]$\times$ (${\it prob}$:$a$:Id fp$\rightarrow$ FinProbSpace
\\[0ex]$\times$ Top))
\-
\end{tabbing}